\begin{tabbing}
$\forall$${\it es}$:ES, $L$:(Id List).
\\[0ex]fischer($L$)
\\[0ex]$\Rightarrow$ \=($\forall$$e_{1}$:E, $j$:Id.\+
\\[0ex]Try($e_{1}$) $\Rightarrow$ ($j$ $\in$ $L$) $\Rightarrow$ ($\neg$($j$ = loc($e_{1}$))) $\Rightarrow$ (the rcv(wanted message from $e_{1}$ to $j$) $\in$ E))
\-
\end{tabbing}